Inference at * 1 2 2 2 
Iof proof for Lemma mul cancel in eq:



1. a : 
2. b : 
3. n : 
4. m:. ((m * a) = (m * b))  (a = b)
5. (n * a) = (n * b)
6. (n > 0)
7. ((-n) * (-a)) = ((-n) * (-b))
  a = b 

latex

 by ((InstHyp [-n] 4) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: .....set predicate..... NILNIL

C1:   0 < (-n)
C.

Definitions	t  T, , False, i > j, A, P  Q, x:A. B(x),
Lemmas	nat plus wf, member wf